/LMAR=0/XLINE=3/FONT#0=BASL30/FONT#1=BASB30/FONT#2=ASI30[LSP,JRA]/FONT#3=SUB/FONT#7=SUP/FONT#12=NGB30/FONT#13=GERM35/FONT#14=MG[LSP,JRA]/FONT#15=GRK30/FONT#4=GRFX35
␈↓ ↓H␈↓␈↓↓  CONTENTS␈↓ X␈↓


␈↓ ↓H␈↓↓␈↓ ∧ZT A B L E   O F   C O N T E N T S



␈↓ ↓H␈↓↓SECTION␈↓ ¬PAGE␈↓
␈↓ ↓H␈↓␈↓↓␈↓ ↔     1␈↓


␈↓ ↓H␈↓A formal theory ␈↓
T␈↓ is defined when the following conditions are satisfied␈↓π 1␈↓:

␈↓ ↓H␈↓␈↓ α_␈↓↓1.␈↓␈α⊂A␈α⊂countable␈α⊂set␈α⊂of␈α⊂symbols␈α⊂is␈α⊃given␈α⊂as␈α⊂the␈α⊂symbols␈α⊂of␈α⊂␈↓
T␈↓.␈α⊂ A␈α⊂finite␈α⊃sequence␈α⊂of
␈↓ ↓H␈↓␈↓ α_symbols of ␈↓
T␈↓ is called an expression of ␈↓
T␈↓.

␈↓ ↓H␈↓␈↓ α_␈↓↓2.␈↓␈α↔There␈α⊗is␈α↔a␈α⊗subset␈α↔of␈α⊗the␈α↔expressions␈α⊗of␈α↔␈↓
T␈↓␈α⊗called␈α↔the␈α↔␈↓αwell-formed␈α⊗formulas␈↓
␈↓ ↓H␈↓␈↓ α_(abbreviated ␈↓αwffs␈↓) of ␈↓
T␈↓␈↓π 2␈↓.

␈↓ ↓H␈↓␈↓ α_␈↓↓3.␈↓ A set of wffs is set aside and cslled the set of ␈↓αaxioms␈↓ of ␈↓
T␈↓␈↓π 3␈↓.

␈↓ ↓H␈↓␈↓ α_␈↓↓4.␈↓␈αTher␈αis␈αa␈αfinite␈αset␈αof␈αrelations␈α␈↓
R␈↓β1␈↓, ... ,␈↓
R␈↓βn␈↓␈αon␈αwffs,␈αcalled␈α␈↓αrules␈αof␈αinference␈↓.␈αFor␈αeach
␈↓ ↓H␈↓␈↓ α_␈↓
R␈↓βi␈↓␈αthere␈αis␈αa␈αunique␈αpositve␈αinteger␈α␈↓
j␈↓␈αsuch␈αthat␈αfor␈αevery␈αset␈αof␈α␈↓
j␈↓␈αwffs␈αand␈αeach␈αwff␈α␈↓A␈↓
␈↓ ↓H␈↓␈↓ α_one␈αcan␈αeffectively␈αdecise␈αwhether␈αthe␈αgiven␈α␈↓
j␈↓␈αwffs␈αare␈αin␈αthe␈αrelation␈α␈↓
R␈↓βi␈↓␈αto␈α␈↓A␈↓,␈αand,␈αif
␈↓ ↓H␈↓␈↓ α_so ␈↓A␈↓ is called a ␈↓αdirect consequence␈↓ of the given wffs by virtue of ␈↓
R␈↓βi␈↓.

␈↓ ↓H␈↓Let␈α
␈↓∂G␈↓␈α
be␈α
a␈α
set␈α
of␈α
wffs,␈α
and␈α
let␈α
␈↓P␈↓␈α
be␈α
a␈α
wff␈α
in␈α
the␈α
formal␈α
theory␈α
␈↓
T␈↓.␈α
 We␈α
say␈α
␈↓P␈↓α␈α
is␈α
deducible␈α∞for␈α
␈↓∂G␈↓
␈↓ ↓H␈↓(denoted␈α␈↓∂G␈↓∧ε␈↓P␈↓)␈αif␈αthere␈αexists␈αa␈αfinite␈αsequence␈αof␈αwffs␈α␈↓P␈↓β1␈↓, ..., ␈↓P␈↓βn␈↓␈αsuch␈αthat␈α␈↓P␈↓βn␈↓ = ␈↓P␈↓␈αand␈αfor␈α1≤i≤n,␈α␈↓P␈↓βi␈↓
␈↓ ↓H␈↓is either an axiom, a formula in ␈↓∂G␈↓ is a direct



















␈↓ ↓H␈↓________________
␈↓ ↓H␈↓␈↓π 1␈↓ See page page  for propositional logic as a formal theory.

␈↓ ↓H␈↓␈↓ α_␈↓π 2␈↓␈αTher␈αis␈αusually␈αan␈αeffective␈αprocedure␈αto␈αdetermine␈αwhether␈αa␈αgiven␈αexpression␈αis␈αa
␈↓ ↓H␈↓␈↓ α_wff.

␈↓ ↓H␈↓␈↓ α_␈↓π 3␈↓␈α␈↓
T␈↓␈αis␈αan␈αaxiomatic␈αtheory␈αif␈αthere␈αexists␈αan␈αeffective␈αprocedure␈αfor␈αdeciding␈αwhether
␈↓ ↓H␈↓␈↓ α_a given wff is an axiom.